R-Feasible(ecl-machine at "b" with state ecl

R-Feasible(eclcatch([eclseq(ecland(eclbase(rcv(lnk1{input to b},"play");s,v.
R-Feasible(true);eclbase(locl("choose1");s,v. true));eclor(eclthrow(eclbase(locl("diff");s,v.
R-Feasible(true);1);eclbase(locl("same");s,v. true)))]*;[1]).1

R-Feasible(state variables "x1" : 3  "v1" : 3  "win" :   "x2" : 3  "v2" : 3

R-Feasible(actions rcv(lnk1{input to b},"play") : 3  locl("choose1") : Unit  
R-Feasible(actions locl("diff") : Unit  locl("same") : Unit  rcv(lnk1{b to output},"hello") : 

R-Feasible(sends locl("diff") sends on lnk1{b to output}
R-Feasible(sends lwith tag "hello" [s,v.rps(s("x1");s("v1"))], at marker 1

R-Feasible(updates update-spec1(locl("diff");"win";1;s,v.s("win")+if rps(s("x1");s("v1")) 1
R-Feasible(updates update-spec1(locl("diff");"win";1;s,v.s("win")+else 0 fi)
 (@"b" precondition for "diff"(v:Unit):
 (@"b" s,v. s("x1") = s("v1")   State("x1" : 3  "v1" : 3) v
  @"b" precondition for "same"(v:Unit):
  @"b" s,v. s("x1") = s("v1")   State("x1" : 3  "v1" : 3) v)
 @"b" precondition for "choose1"(v:Unit):
 @"b" s,v. True State() v
 @"b" effect rcv(lnk1{input to b},"play")(v:3)  "x1" := s,v. v State("x1" : 3) v 
 @"b" effect locl("choose1")(v:Unit)  "v1" := s,v. random(0;2) State("v1" : 3) v ) 

latex

Definitions

P & Q, Top, t  T, A & B, "$x", f  g, IdDeq, x : v, {i..j}, KindDeq, rcv(l,tg), lnk$n{$a to $b}, locl(a), a.n, eclcatch(a;l), [a]*, eclseq(a;b), ecland(a;b), eclbase(k;test), true, eclor(a;b), eclthrow(a;n), if b t else f fi, x:A. B(x), Id, P  Q, xL. P(x), ecl-kinds(x), b, destination(l), x  dom(f), A, x. t(x), IdLnk, , AB, False, Prop, x,y. t(x;y), eqof(d), union-deq(A;B;a;b), product-deq(A;B;a;b), IdLnkDeq, 1of(t), sumdeq(a;b), false, p  q, a = b, a = b, Atom2Deq, eq_atom$n(x;y), proddeq(a;b), 2of(t), i  j < k, b, Normal(T), ecl ind, Y, as @ bs, l[i], SQType(T), {T}, hd(l), nth_tl(n;as), ij, tl(l), i<j, True, deq-member(eq;x;L), reduce(f;k;as), p  q, filter(P;l), source(l), R-Feasible(R), , A || B, Normal(ds), Dec(P), P  Q, P  Q, Rplus?(x1), Rplus-left(x1), Rplus-right(x1), Rnone?(x1), R-loc(R), Rds(R), Rda(R), p = q, R-base-domain(R), R-frame-compat(A;B), R-interface-compat(A;B), i=j, Reffect?(x1), Rframe?(x1), Rframe-x(x1), Reffect-x(x1), Reffect-knd(x1), Rframe-L(x1), Raframe?(x1), Raframe-k(x1), Raframe-L(x1), Rrframe?(x1), Rrframe-x(x1), Reffect-ds(x1), Rrframe-L(x1), Rsends?(x1), Rsframe?(x1), Rsframe-lnk(x1), Rsends-l(x1), Rsframe-tag(x1), Rsends-g(x1), Rsends-knd(x1), Rsframe-L(x1), Rbframe?(x1), Rbframe-k(x1), Rbframe-L(x1), Rsends-ds(x1), Rpre?(x1), Rpre-ds(x1), Rpre-a(x1), Rsends-dt(x1), Reffect-T(x1), Rsends-T(x1), P  Q, DeclaredType(ds;x), Unit, f(x)?z, f(x), , Knd, x(s), State(ds), x(s1,s2), (x  l), x:A. B(x), ||as||, , a = b, State(ds)

Lemmas

R-Feasible-Rplus, ecl-feasible, fpf-join wf, Id wf, fpf-single wf, int seg wf, id-deq wf, Knd wf, rcv wf, locl wf, unit wf, Kind-deq wf, bool wf, eclact wf, eclcatch wf, eclrepeat wf, eclseq wf, ecland wf, eclbase wf, btrue wf, ma-valtype wf, decl-state wf, eclor wf, eclthrow wf, le wf, nat wf, msg-spec1 wf, fpf-join-cap-sq, top wf, fpf-cap-single, fpf-single-dom-sq, eqof eq btrue, update-spec1 wf, eq id wf, iff transitivity, assert wf, eqtt to assert, assert-eq-id, ifthenelse wf, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, rps wf, fpf-cap-single-join, subtype rel self, deq wf, normal-ds-join, normal-ds-single, normal-da-join, normal-da-single, it wf, bool-inhabited, Knd sq, decidable int equal, true wf, false wf, isrcv wf, select wf, length wf1, l member wf, update-spec1-decl, msg-spec-loc-decl-spec1, decidable ex unit, decidable not, fpf-compatible-self, fpf-compatible-singles, fpf-all-empty, fpf-empty wf, assert-eq-knd, Rpre wf, Rplus wf, Reffect wf, fpf-cap-single1, random wf, R-compat-symmetry, R-compat-Rplus-sq, fpf-empty-compatible-right, fpf-empty-compatible-left, fpf-compatible-join, ecl-machine wf, ecl-precond-compatible, fpf-compatible-join2